Inference at * 1 1 1 2 2 
Iof proof for Lemma comp nat ind tp:

.....wf..... NILNIL

1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. i : 
  i   

latex

 by MemEqCD 

latex

 .

Definitions

t  T